FDL - Step of Proof: complete_nat_ind_with_y

Step of Proof: complete_nat_ind_with_y

Inference at *
Iof proof for Lemma complete nat ind with y:

P:(

{k}). (

i:

. (

j:

i. P(j))

P(i))

(

i:

. P(i))

by UseWitness

P,g. Y(

f,x. g(x,f))

1:

1:

(

P,g. Y(

f,x. g(x,f)))

(

P:(

{k}). (

i:

. (

j:

i. P(j))

P(i))

(

i:

. P(i)))

.

Definitions t T